1. Field of the Invention
The present invention relates to computer systems and methods for evaluating, verifying and testing software program logic. More particularly, the invention concerns the use of weakest precondition analysis (or other forms of symbolic analysis) for object-oriented programs that support dynamic dispatch of functions and methods.
2. Description of the Prior Art
By way of background, weakest precondition (wp) analysis is a type of symbolic analysis that deals with the problem of finding a precondition φ that necessarily drives a software program from a particular entry point m to a goal state g. For example, g might represent some behavior of a library, such as a particular line of code throwing an exception. The discovered precondition φ could illustrate how to make such behavior occur when the library code is invoked. This type of analysis has numerous applications in tools for software engineering, including but not limited to (1) specification discovery and API (Application Program Interface) hardening, (2) bug validation, and (3) test case generation.
Real-world programs present many challenges for wp analysis. One problem arises from the sheer scale of large programs. Even in loop-free programs, wp analysis faces an exponential explosion due to the number of distinct paths through the program. In straight-line code alone, handling language features such as aliasing and type tests can require logical disjunctions, another source of state explosion.
Procedure calls further exacerbate these difficulties and introduce entirely new challenges stemming from the need to generate a call graph for interprocedural analysis. This is especially problematic for large object-oriented libraries and frameworks. For object-oriented programs, which support polymorphism and dynamic dispatch, performing the interprocedural analysis requires determining the possible targets of virtual method calls. Unfortunately, standard call graph construction algorithms face myriad difficulties disambiguating virtual calls in real-world libraries, due to the scale of the programs, unknown aliasing that clients might establish, and dynamic language features like reflection.
There is therefore a need for a software analysis technique that provides a new approach to wp analysis (and other forms of symbolic analysis), particularly for large object-oriented software environments.